<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" />
  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>Index &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script src="_static/jquery.js?v=5d32c60e"></script>
        <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
        <script src="_static/documentation_options.js?v=7048e04d"></script>
        <script src="_static/doctools.js?v=9a2dae69"></script>
        <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="#" />
    <link rel="search" title="Search" href="search.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul class="current">
<li class="toctree-l1 current"><a class="current reference internal" href="#">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active">Index</li>
      <li class="wy-breadcrumbs-aside">
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             

<h1 id="index">Index</h1>

<div class="genindex-jumpbox">
 <a href="#A"><strong>A</strong></a>
 | <a href="#B"><strong>B</strong></a>
 | <a href="#C"><strong>C</strong></a>
 | <a href="#D"><strong>D</strong></a>
 | <a href="#E"><strong>E</strong></a>
 | <a href="#F"><strong>F</strong></a>
 | <a href="#G"><strong>G</strong></a>
 | <a href="#H"><strong>H</strong></a>
 | <a href="#I"><strong>I</strong></a>
 | <a href="#L"><strong>L</strong></a>
 | <a href="#M"><strong>M</strong></a>
 | <a href="#N"><strong>N</strong></a>
 | <a href="#O"><strong>O</strong></a>
 | <a href="#P"><strong>P</strong></a>
 | <a href="#R"><strong>R</strong></a>
 | <a href="#S"><strong>S</strong></a>
 | <a href="#T"><strong>T</strong></a>
 | <a href="#U"><strong>U</strong></a>
 | <a href="#V"><strong>V</strong></a>
 
</div>
<h2 id="A">A</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C09_Groups_and_Rings.html#index-3">abel</a>
</li>
      <li><a href="C02_Basics.html#index-24">absolute value</a>
</li>
      <li><a href="C03_Logic.html#index-17">absurd</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-7">anonymous constructor</a>
</li>
      <li><a href="C02_Basics.html#index-12">apply</a>, <a href="C02_Basics.html#index-17">[1]</a>
</li>
      <li><a href="C03_Logic.html#index-19">assumption</a>
</li>
  </ul></td>
</tr></table>

<h2 id="B">B</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C04_Sets_and_Functions.html#index-3">bounded quantifiers</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-23">by_cases</a>
</li>
      <li><a href="C03_Logic.html#index-14">by_contra</a>
</li>
  </ul></td>
</tr></table>

<h2 id="C">C</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-3">calc</a>
</li>
      <li><a href="C03_Logic.html#index-8">cases</a>
</li>
      <li><a href="C03_Logic.html#index-2">change</a>
</li>
      <li><a href="C01_Introduction.html#index-0">check</a>
</li>
      <li>
    command

      <ul>
        <li><a href="C02_Basics.html#index-9">open</a>
</li>
      </ul></li>
      <li>
    commands

      <ul>
        <li><a href="C01_Introduction.html#index-0">check</a>
</li>
      </ul></li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-8">commutative ring</a>
</li>
      <li><a href="C03_Logic.html#index-25">congr</a>
</li>
      <li><a href="C03_Logic.html#index-18">constructor</a>
</li>
      <li><a href="C11_Topology.html#index-3">continuity</a>
</li>
      <li><a href="C03_Logic.html#index-17">contradiction</a>
</li>
      <li><a href="C03_Logic.html#index-16">contrapose</a>
</li>
      <li><a href="C03_Logic.html#index-26">convert</a>
</li>
  </ul></td>
</tr></table>

<h2 id="D">D</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C05_Elementary_Number_Theory.html#index-0">decide</a>
</li>
      <li><a href="C02_Basics.html#index-13">definitional equality</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C12_Differential_Calculus.html#index-0">differential calculus</a>
</li>
      <li><a href="C02_Basics.html#index-25">divisibility</a>
</li>
      <li><a href="C03_Logic.html#index-2">dsimp</a>
</li>
  </ul></td>
</tr></table>

<h2 id="E">E</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C12_Differential_Calculus.html#index-1">elementary calculus</a>
</li>
      <li><a href="C03_Logic.html#index-4">erw</a>
</li>
      <li><a href="C02_Basics.html#index-12">exact</a>, <a href="C02_Basics.html#index-17">[1]</a>, <a href="C02_Basics.html#index-5">[2]</a>
</li>
      <li><a href="C03_Logic.html#index-22">excluded middle</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-17">exfalso</a>
</li>
      <li><a href="C02_Basics.html#index-19">exponential</a>
</li>
      <li><a href="C03_Logic.html#index-24">ext</a>
</li>
      <li><a href="C03_Logic.html#index-24">extensionality</a>
</li>
  </ul></td>
</tr></table>

<h2 id="F">F</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-11">field_simp</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C11_Topology.html#index-1">Filter</a>
</li>
      <li><a href="C03_Logic.html#index-12">from</a>
</li>
  </ul></td>
</tr></table>

<h2 id="G">G</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-26">gcd</a>
</li>
      <li><a href="C02_Basics.html#index-2">goal</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-14">group (algebraic structure)</a>, <a href="C09_Groups_and_Rings.html#index-1">[1]</a>

      <ul>
        <li><a href="C02_Basics.html#index-15">(tactic)</a>, <a href="C09_Groups_and_Rings.html#index-2">[1]</a>
</li>
      </ul></li>
  </ul></td>
</tr></table>

<h2 id="H">H</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-11">have</a>, <a href="C03_Logic.html#index-12">[1]</a>
</li>
  </ul></td>
</tr></table>

<h2 id="I">I</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-10">implicit argument</a>
</li>
      <li><a href="C02_Basics.html#index-16">inequalities</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-5">injective function</a>
</li>
      <li><a href="C13_Integration_and_Measure_Theory.html#index-0">integration</a>, <a href="C13_Integration_and_Measure_Theory.html#index-1">[1]</a>
</li>
      <li><a href="C03_Logic.html#index-0">intro</a>
</li>
  </ul></td>
</tr></table>

<h2 id="L">L</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-1">lambda abstraction</a>
</li>
      <li><a href="C02_Basics.html#index-28">lattice</a>
</li>
      <li><a href="C02_Basics.html#index-26">lcm</a>
</li>
      <li><a href="C03_Logic.html#index-21">left</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-13">let</a>
</li>
      <li><a href="C02_Basics.html#index-18">linarith</a>
</li>
      <li><a href="C10_Linear_Algebra.html#index-1">linear map</a>
</li>
      <li><a href="C02_Basics.html#index-2">local context</a>
</li>
      <li><a href="C02_Basics.html#index-19">logarithm</a>
</li>
  </ul></td>
</tr></table>

<h2 id="M">M</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C10_Linear_Algebra.html#index-3">matrices</a>
</li>
      <li><a href="C02_Basics.html#index-21">max</a>
</li>
      <li><a href="C13_Integration_and_Measure_Theory.html#index-2">measure theory</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-30">metric space</a>, <a href="C11_Topology.html#index-2">[1]</a>
</li>
      <li><a href="C02_Basics.html#index-21">min</a>
</li>
      <li><a href="C09_Groups_and_Rings.html#index-0">monoid</a>
</li>
      <li><a href="C03_Logic.html#index-3">monotone function</a>
</li>
  </ul></td>
</tr></table>

<h2 id="N">N</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-9">namespace</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-20">norm_num</a>
</li>
      <li><a href="C12_Differential_Calculus.html#index-2">normed space</a>
</li>
  </ul></td>
</tr></table>

<h2 id="O">O</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-9">open</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-27">order relation</a>
</li>
  </ul></td>
</tr></table>

<h2 id="P">P</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-27">partial order</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-2">proof state</a>
</li>
      <li><a href="C03_Logic.html#index-15">push_neg</a>
</li>
  </ul></td>
</tr></table>

<h2 id="R">R</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-9">rcases</a>
</li>
      <li><a href="C02_Basics.html#index-1">real numbers</a>
</li>
      <li><a href="C02_Basics.html#index-13">reflexivity</a>
</li>
      <li><a href="C02_Basics.html#index-23">repeat</a>
</li>
      <li><a href="C02_Basics.html#index-0">rewrite</a>
</li>
      <li><a href="C02_Basics.html#index-13">rfl</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-21">right</a>
</li>
      <li><a href="C02_Basics.html#index-7">ring (algebraic structure)</a>, <a href="C09_Groups_and_Rings.html#index-4">[1]</a>

      <ul>
        <li><a href="C02_Basics.html#index-6">(tactic)</a>
</li>
      </ul></li>
      <li><a href="C03_Logic.html#index-9">rintro</a>
</li>
      <li><a href="C02_Basics.html#index-0">rw</a>, <a href="C02_Basics.html#index-4">[1]</a>
</li>
      <li><a href="C04_Sets_and_Functions.html#index-2">rwa</a>
</li>
  </ul></td>
</tr></table>

<h2 id="S">S</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C04_Sets_and_Functions.html#index-0">set operations</a>
</li>
      <li><a href="C02_Basics.html#index-22">show</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-20">simp</a>, <a href="C04_Sets_and_Functions.html#index-1">[1]</a>
</li>
      <li><a href="C03_Logic.html#index-10">surjective function</a>
</li>
  </ul></td>
</tr></table>

<h2 id="T">T</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li>
    tactics

      <ul>
        <li><a href="C02_Basics.html#index-15">abel</a>, <a href="C09_Groups_and_Rings.html#index-3">[1]</a>
</li>
        <li><a href="C02_Basics.html#index-12">apply</a>, <a href="C02_Basics.html#index-17">[1]</a>
</li>
        <li><a href="C03_Logic.html#index-19">assumption</a>
</li>
        <li><a href="C03_Logic.html#index-23">by_cases</a>
</li>
        <li><a href="C03_Logic.html#index-14">by_contra and by_contradiction</a>
</li>
        <li><a href="C02_Basics.html#index-3">calc</a>
</li>
        <li><a href="C03_Logic.html#index-8">cases</a>
</li>
        <li><a href="C03_Logic.html#index-2">change</a>
</li>
        <li><a href="C03_Logic.html#index-25">congr</a>
</li>
        <li><a href="C03_Logic.html#index-18">constructor</a>
</li>
        <li><a href="C11_Topology.html#index-3">continuity</a>
</li>
        <li><a href="C03_Logic.html#index-17">contradiction</a>
</li>
        <li><a href="C03_Logic.html#index-16">contrapose</a>
</li>
        <li><a href="C03_Logic.html#index-26">convert</a>
</li>
        <li><a href="C05_Elementary_Number_Theory.html#index-0">decide</a>
</li>
        <li><a href="C03_Logic.html#index-2">dsimp</a>
</li>
        <li><a href="C03_Logic.html#index-4">erw</a>
</li>
        <li><a href="C02_Basics.html#index-12">exact</a>, <a href="C02_Basics.html#index-17">[1]</a>, <a href="C02_Basics.html#index-5">[2]</a>
</li>
        <li><a href="C03_Logic.html#index-17">exfalso</a>
</li>
        <li><a href="C03_Logic.html#index-24">ext</a>
</li>
        <li><a href="C03_Logic.html#index-11">field_simp</a>
</li>
        <li><a href="C03_Logic.html#index-12">from</a>
</li>
        <li><a href="C02_Basics.html#index-15">group</a>, <a href="C09_Groups_and_Rings.html#index-2">[1]</a>
</li>
        <li><a href="C02_Basics.html#index-11">have</a>, <a href="C03_Logic.html#index-12">[1]</a>
</li>
        <li><a href="C03_Logic.html#index-0">intro</a>
</li>
        <li><a href="C03_Logic.html#index-21">left</a>
</li>
        <li><a href="C03_Logic.html#index-13">let</a>
</li>
        <li><a href="C02_Basics.html#index-18">linarith</a>
</li>
        <li><a href="C02_Basics.html#index-15">noncomm_ring</a>
</li>
        <li><a href="C02_Basics.html#index-20">norm_num</a>
</li>
        <li><a href="C03_Logic.html#index-15">push_neg</a>
</li>
        <li><a href="C03_Logic.html#index-9">rcases</a>
</li>
        <li><a href="C02_Basics.html#index-13">refl and reflexivity</a>
</li>
        <li><a href="C02_Basics.html#index-23">repeat</a>
</li>
        <li><a href="C03_Logic.html#index-21">right</a>
</li>
        <li><a href="C02_Basics.html#index-6">ring</a>
</li>
        <li><a href="C03_Logic.html#index-9">rintro</a>
</li>
        <li><a href="C02_Basics.html#index-0">rw and rewrite</a>, <a href="C02_Basics.html#index-4">[1]</a>
</li>
        <li><a href="C04_Sets_and_Functions.html#index-2">rwa</a>
</li>
        <li><a href="C02_Basics.html#index-22">show</a>
</li>
        <li><a href="C03_Logic.html#index-20">simp</a>, <a href="C04_Sets_and_Functions.html#index-1">[1]</a>
</li>
        <li><a href="C02_Basics.html#index-29">trans</a>
</li>
        <li><a href="C03_Logic.html#index-6">use</a>
</li>
      </ul></li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-12">this</a>
</li>
      <li><a href="C11_Topology.html#index-4">topological space</a>
</li>
      <li><a href="C11_Topology.html#index-0">topology</a>
</li>
      <li><a href="C02_Basics.html#index-29">trans</a>
</li>
  </ul></td>
</tr></table>

<h2 id="U">U</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-6">use</a>
</li>
  </ul></td>
</tr></table>

<h2 id="V">V</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C10_Linear_Algebra.html#index-0">vector space</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C10_Linear_Algebra.html#index-2">vector subspace</a>
</li>
  </ul></td>
</tr></table>



           </div>
          </div>
          <footer>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>